/** ================================================= 
 *  Evaluator for the untyped lambda calculus using
 *  The de Bruijn notation for lambda-terms
 * =================================================
 */ 

/* domain 
 	Dom_Const = Const &
 	Dom_Var = Var &
 	Dom_Abstr = Abstr &
 	Dom_App = App
 */   
   
/** =================================================
 *      Lambda Terms for Untyped Lambda Calculus
 *  =================================================
 */

sealed abstract class Term {
  def isSame(t: Term): Boolean = (this: Term) match {
    case Const() => t.isInstanceOf[Const]
    
    case Var(x: Int) => (t : Term) match {
      case Var(y: Int) => x == y
      case _ if !t.isInstanceOf[Var] => false
    }
    
    case Abstr(t1: Term) => (t: Term) match {
      case Abstr(t2: Term) => t1.isSame(t2)
      case _ if !t.isInstanceOf[Abstr] => false
    }
      
    case App(t1: Term, t2: Term) => (t: Term) match {
      case App(t21: Term, t22: Term) => t1.isSame(t21) && t2.isSame(t22)
      case _ if !t.isInstanceOf[App] => false
    }
  }
}

class Const extends Term
class Var(val index: Int) extends Term
class Abstr(val t: Term) extends Term
class App(val t1: Term, val t2: Term) extends Term

/** =================================================
 *           Extractors for the Lambda Terms
 *  =================================================
 */

object Const {
  def apply(): Const = new Const()
  def unapply(c: Const): Boolean = true
}

object Var {
  def apply(index: Int): Var = new Var(index)
  def unapply(v: Var): Option[Int] = Some(v.index)
}
object Abstr {
  def apply(t: Term): Abstr = new Abstr(t)
  def unapply(a: Abstr): Option[Term] = 
    Some(a.t)
}
object App {
  def apply(t1: Term, t2: Term): App = new App(t1,t2)
  def unapply(a: App): Option[(Term,Term)] = 
    Some(Tuple2(a.t1,a.t2))
}




/** =================================================
 *                 Lambda Terms Evaluator
 *		       CallByValue
 *  =================================================
 */


class Eval {
  
  def reduce(t: Term): Term =
    if(this.reduceCallByValue(t).isSame(t)) { t }
    else { this.reduce(this.reduceCallByValue(t)) }
  
  def isValue(t: Term): Boolean =
    /* postcondition   t \in Abstr <--> res == true
    */
    t.isInstanceOf[Term]  /** XXX: It doesn't match the specifiction */
  
  def reduceCallByValue(t: Term): Term = (t : Term) match {
      
    case App(Abstr(t1:Term),v2:Term) if this.isValue(v2) =>
      this.subst(t1,1,v2)
  
    case App(v1: Abstr, t2: Term) if !this.isValue(t2) =>
      App(v1, this.reduceCallByValue(t2))

    case App(t1: Term, t2: Term) if !this.isValue(t1) =>
      App(this.reduceCallByValue(t1), t2)
	
    case Abstr(t1: Term) => Abstr(this.reduceCallByValue(t1))
    case Var(_) => t
    case Const() => t
  }
  
  def subst(t: Term, index: Int, s: Term): Term = (t: Term) match {
    case Const() => t
    
    case Var(y: Int) =>
      if (y == index) { s } else { t }
    
    case Abstr(t1: Term) => Abstr(this.subst(t1,index+1,s))
      
    case App(t1: Term, t2: Term) =>
      App(this.subst(t1,index,s), this.subst(t2,index,s))
  }
  
}

/** =================================================
 *             Printer for Lambda Terms
 *  =================================================
 

class Printer {
  def prompt(t: Term): Unit = {
    printer(t)
    println
  }
  def printer(t: Term): Unit = (t: Term) match {
    case Var(x) => print(x)
    case Abstr(t) => print("\\. ("); printer(t); print(")")
    case App(t1,t2) => print("("); printer(t1); print(") ");
                       print("("); printer(t2); print(") ");
  }
}
*/

/** =================================================
 *   \\z. (\\y. y (\\x. x)) (\\x. z x) 
 *   is in de Bruijn notation
 *   \\ (\\ 1 (\\ 1)) (\\ 2 1)
 *   and it evaluates to:
 *   \\ 2 (\\ 1) that is \\z. z (\\x. x)
 *  =================================================
 */ 
object Untyped {

   def main(args: Array[String]): Unit =
   /**new Printer().prompt(*/
     new Eval().reduce(
       Abstr(
         App(
           Abstr(App(Var(1), Abstr(Var(1)))),
           Abstr(App(Var(2),Var(1)))
         )
       )
     )
   /**)*/
}